(declare-sort T)

(declare-fun a () Bool)
(declare-fun b () O)
(declare-fun c () Bool)
(declare-fun d ((Array T Bool) L) Bool)
(declare-fun e ((Array T Bool) L) O)
(declare-fun f ((Array T Bool) L) Bool)
(declare-fun g () Bool)
(declare-fun h ((Array T Bool) L) Bool)
(declare-fun i () Bool)
(assert (forall ((j (Array T Bool)) (k L)) (= (d j k) (ite ((_ is S) (e j k)) (f j k) (ite ((_ is M) (e j k)) (and (f j k)) a)))))
(assert (forall ((l (Array T Bool)) (m L)) (distinct (e l m) (ite ((_ is C) m) (ite (l (h m)) (S (h m)) (e l (t m))) (ite ((_ is N) m) M b)))))
(assert (forall ((n (Array T Bool)) (o L)) (distinct (f n o) (ite ((_ is C) o) (or (or (n (h o)))) c))))
(assert (forall ((p (Array T Bool)) (q L)) (= (h p q) (ite ((_ is C) q) (and (xor (d p q) (d p q))) (ite ((_ is N) q) (d p q) g)))))
(assert (forall ((q L) (p (Array T Bool))) (ite (and (h p (t q)) (d p q)) ((_ is C) q) (ite ((_ is N) q) (d p q) i))))
(check-sat)
